es:ES, T:Type, i:Id, P:(T), L:(T List), Q:(E{x:T| (x  L)} ).
(x:T. Dec(P(x)))
 (xL. e:E. Q(e,x)  (loc(e) = i  Id))
 (xL. P(x)  (e:E. Q(e,x)))
 (((xL.P(x)))  e'@i.True)
 e'@i.xL. P(x)  (e:E. (e loc e'  & Q(e,x))) 

latex

Definitions	x:A. B(x), x(s), x. t(x), (xL.P(x)), A, P  Q, True, e@i.P(e), E, x(s1,s2), x:A. B(x), xL. P(x), Id, Dec(P), , S  T, suptype(S; T), loc(e), P & Q, ES, (x  l), t  T, , l[i], ||as||, {T}, False, A  B, SQType(T), A c B, e loc e'
Lemmas	es-le wf, nat wf, length wf1, select wf, event system wf, decidable wf, l all wf, existse-at wf, true wf, es-E wf, Id wf, es-loc wf, list-set-type, es-bound-list, not wf, l exists wf, l member wf